from z3 import *

# Z 代表整数类型
Z = IntSort()

B = BoolSort()
f = Function("f", B, Z)
g = Function("g", Z, B)
a = Bool("a")

# 求解一个公式
solve(g(1 + f(a)))
# > [a = False, f = [else -> 0], g = [else -> True]]

x = Int("x")
y = Int("y")

# n 是一个术语，表示一个布尔表达式
n = x + y >= 3
print("num args: ", n.num_args())
print("children: ", n.children())
print("1st child:", n.arg(0))
print("2nd child:", n.arg(1))
print("operator: ", n.decl())
print("op name:  ", n.decl().name())
# > num args:  2
# > children:  [x + y, 3]
# > 1st child: x + y
# > 2nd child: 3
# > operator:  >=
# > op name:   >=
